#!/bin/bash

##################
# Return values:
# 1: parameters or files error
# 2: SAT Solver error
# 10: CPU and GPU solvers outputs match (passed)
# 20: CPU and GPU solvers outputs do not match (failed)
#
##################

# Temporary files
DATE=`date +"%y_%m_%d_%H_%M_%S"`
TMP_FILE=/tmp/test_cnf_${DATE}_${RANDOM}
TMP_CNF=/tmp/test_cnf_cpu_${DATE}_${RANDOM}

# Input files
CNF=$1
SOLUTION_TO_CHECK=$2

# Executables
CUDAPSAT=../Debug/GPUSATSolver
MINISAT=../../../../minisat/core/minisat

if [[ "$#" != 2 ]]
then
	echo "Wrong number of parameters. Expected 2." >&2
	exit 1
fi

if ! [[ -e "$CNF" ]]
then
	echo "Could not find the CNF file." >&2
	exit 1
fi

if ! [[ -e "$SOLUTION_TO_CHECK" ]]
then
	echo "Could not find the solution file." >&2
	exit 1
fi


VARIABLES=`cat $CNF | grep "p cnf" | cut -d " " -f 3`
CLAUSES=`cat $CNF | grep "p cnf" | cut -d " " -f 4`

SAT=`cat $SOLUTION_TO_CHECK | egrep "SAT|UNSAT|UNDEF"`
SOLUTIONS=(`cat $SOLUTION_TO_CHECK | egrep -x "((-)?[1-9][0-9]* )+0"`)


if [[ $SAT != "UNDEF" ]] && [[ $SAT != "UNSAT" ]] && [[ $SAT != "SAT" ]]
then

	echo "GPU SAT Solver returned an unknown output." >&2
	exit 2

fi

if [[ $SAT == "UNDEF" ]]
then
	echo "CUDA SAT Solver did not return answer..." >&2
	exit 2
fi

if [[ $SAT == "UNSAT" ]]
then

	$MINISAT $CNF 2>&1 > /dev/null
	RESULT=$?

	if [[ $RESULT != "10" ]] && [[ $RESULT != "20" ]]
	then
		echo "An error has occurred on the CPU SAT Solver"
		exit 2
	fi

	if [[ $RESULT == "10" ]]
	then
		echo "NOT MATCHED"
		echo "GPU returns UNSAT while CPU returns SAT"
		exit 20
	fi

	if [[ $RESULT == "20" ]]
	then
		echo "MATCHED"
                echo "Both CPU and GPU return UNSAT"
		exit 10
	fi



else

	cp $CNF $TMP_CNF

	INDEX=0
	LIT=${SOLUTIONS[$INDEX]}

	NUMBER_OF_LITERALS_FOUND=0

	while [ $LIT -ne "0" ]
	do
		echo "$LIT 0" >> $TMP_CNF
		let INDEX++
		LIT=${SOLUTIONS[$INDEX]}
		let NUMBER_OF_LITERALS_FOUND++
	done

	if [[ $NUMBER_OF_LITERALS_FOUND != $VARIABLES ]]
	then
		echo -e "\e[33;1mWarning: The number of variables ($VARIABLES) and literals in the solution ($NUMBER_OF_LITERALS_FOUND) do not match\e[m"
	fi

	$MINISAT $TMP_CNF 2>&1 > /dev/null
	RESULT=$?

	if [[ $RESULT != "10" ]] && [[ $RESULT != "20" ]]
	then
		echo "An error has occurred on the CPU SAT Solver"
		exit 2
	fi

	if [[ $RESULT == "20" ]]
	then
		echo "NOT MATCHED"
		echo "GPU's solution does not satisfy CPU SAT Solver"
		exit 20
	fi

	if [[ $RESULT == "10" ]]
	then
		echo "MATCHED"
                echo "Both CPU and GPU return SAT and solutions match"
		exit 10
	fi


fi

